$\forall$$T$:Type, $l$:($T$ List), $x$:$T$. ($x$ $\in$ $l$) $\Leftarrow\!\Rightarrow$ ($\exists$$l_{1}$,$l_{2}$:$T$ List. ($l$ = ($l_{1}$ @ [$x$] @ $l_{2}$)))